-
Couldn't load subscription status.
- Fork 1.8k
Rust: Non-symmetric type propagation for lub coercions #20592
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Rust: Non-symmetric type propagation for lub coercions #20592
Conversation
1f8f5d3 to
bfea742
Compare
if and matchif and match
2f501e6 to
d0b7388
Compare
if and match61d6041 to
4914a3f
Compare
4a16f67 to
a1fd231
Compare
a1fd231 to
d22f70e
Compare
| toBeTested(x) and not x.isUnknown() and getBody = x.getBody() | ||
| } | ||
|
|
||
| query predicate getClosureBody(ClosureExpr x, Expr getClosureBody) { |
Check warning
Code scanning / CodeQL
Predicates starting with "get" or "as" should return a value Warning generated test
| toBeTested(x) and not x.isUnknown() and getParam = x.getParam(index) | ||
| } | ||
|
|
||
| query predicate getBody(Function x, Expr getBody) { |
Check warning
Code scanning / CodeQL
Predicates starting with "get" or "as" should return a value Warning generated test
|
|
||
| query predicate getBody(Function x, BlockExpr getBody) { | ||
| toBeTested(x) and not x.isUnknown() and getBody = x.getBody() | ||
| query predicate getFunctionBody(Function x, BlockExpr getFunctionBody) { |
Check warning
Code scanning / CodeQL
Predicates starting with "get" or "as" should return a value Warning generated test
d22f70e to
65b706a
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Pull Request Overview
This PR addresses a type inference performance issue in Rust by preventing symmetric type propagation for constructs that use least-upper bound (LUB) coercions, such as if expressions and match arms with multiple branches.
Key Changes:
- Introduced non-symmetric type propagation for LUB coercion contexts to prevent type inference explosions
- Restricted symmetric type equality to single-branch/single-element cases
- Added a test case demonstrating the type inference explosion scenario
Reviewed Changes
Copilot reviewed 3 out of 3 changed files in this pull request and generated 1 comment.
| File | Description |
|---|---|
| rust/ql/lib/codeql/rust/internal/TypeInference.qll | Implements non-symmetric type propagation via new predicates lubCoercion and typeEqualityNonSymmetric, and restricts symmetric propagation for multi-branch constructs |
| rust/ql/test/library-tests/type-inference/main.rs | Adds test case with if expression demonstrating type inference explosion scenario |
| rust/ql/test/library-tests/type-inference/type-inference.expected | Updates expected test output reflecting reduced type inference results due to non-symmetric propagation |
Tip: Customize your code reviews with copilot-instructions.md. Create the file or learn how to get started.
| lubCoercion(mid, n2, suffix) and | ||
| not lubCoercion(mid, n1, _) and |
Copilot
AI
Oct 23, 2025
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The predicate checks lubCoercion(mid, n2, suffix) but doesn't verify that n1 is also a child of mid that would be subject to LUB coercion. This could lead to unintended type propagation paths. Consider adding a check to ensure n1 is also a relevant child of mid when n2 is subject to LUB coercion.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I had the same concern, it looks like n1 is bound by type but not by location in the program.
What would the Rust code this logic targets look like?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
For example, if we have
let x = if b { A } else { C }then
- Type information flows from
AandBto the entireif. - Type information does not flow from
ifto neitherAnorB. - Type information flows in both directions between
ifandx. - If type information can flow from something to
x, then it also flows toA, but only when that something is notB(and vice versa).
Does that make sense?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ah, I was reading typeEquality as "these types are equal" (potentially by coincidence, e.g. two unrelated u32s in the program) whereas it is in fact "these types must be equal" (by type inference). So n1 is in fact quite tightly bound by typeEquality. And I should've read the qldoc for typeEquality.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
DCA is indeed excellent.
Couple of questions and comments.
| lubCoercion(mid, n2, suffix) and | ||
| not lubCoercion(mid, n1, _) and |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I had the same concern, it looks like n1 is bound by type but not by location in the program.
What would the Rust code this logic targets look like?
Rust applies least-upper bound coercions for certain constructs, such as the branches of an
ifexpression, which means that is not sound to propagate type information directly between branches. In fact, doing so can lead to type inference explosions, as witnessed by the example added on this PR.Instead of attempting to model lub coercions, we simply prevent type information to propagate from one branch to another by going directly via the type of the
ifexpression (and similar for other constructs with lub coercions).DCA looks great; we recover the performance lost on #20282 for
ruff,rendiation, andcoreutils.